ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple(ds; da).
ecl-trans-normal(v)
 (L':(event-info(ds;da) List). 
 (L:(event-info(ds;da) List). 
 iseg(event-info(ds;da); L; L')  (ecl-trans-halt2(ds; da; v)(0,L))  False)
  (ecl-trans-state(reset-ecl-tuple(v); L')
  (=
  (ecl-trans-state(v; L')
  ( ecl-trans-type(reset-ecl-tuple(v)))) 

latex

Definitions

Id, t  T, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, ecl-trans-tuple{i:l}(ds; da), ecl-trans-normal(x), event-info(ds;da), A  B, P  Q, False, A, , prop{i:l}, ecl-trans-halt2(ds; da; A), iseg(T; l1; l2), ecl-trans-state(v; L), reset-ecl-tuple(A), ecl-trans-type(A), ma-valtype(da; k), Kind-deq, (x  l), b, b, , deq-member(eq; x; L), P  Q, P  Q, Unit, decl-state(ds), top, fpf-cap(f; eq; x; z), if b then t else f fi , x,y. t(x;y), list_accum(x,a.f(x;a); y; l), append(as; bs), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-state-from(v; z; L), ecl-trans-init(v), subtype(S; T), ecl-trans-h(v)

Lemmas

list accum append, decl-state wf, fpf-cap wf, top wf, list accum functionality, append wf, list accum wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, l member wf, Kind-deq wf, iseg wf, ecl-trans-halt2 wf, false wf, le wf, event-info wf, ecl-trans-normal wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf